%
% Copyright (C) Håkan Lindqvist 2006, 2007.
% May be copied freely for educational and personal use. Any other use
% needs my written consent (i.e. no commercial use without my approval).
%

\newpage
\section{Defining secure systems}
% initial small talk, see Bishop p.31 
One important part of understanding the term ``secure'' is to
understand exactly what that term means in this context. Consider for
example the action of opening a file for writing and then writing some
data to it. Two questions may come from this seemingly simple
action:
Was the subject allowed to access and modify that subject, and can the
system be considered secure after those actions?

Unless explicitly stated, the discussion below is adapted 
from~\cite{Bishop}.

%%%%%% Bishop p.31
\subsection{Protection states}
\label{protection states}
\index{protection state}
To be able to analyze a situation in which the question of whether or
not a system is secure, the system can be thought of as a
state machine in which all components of the system makes up the
definition of each state, and changes in any of these components
constitutes a transition to another state. Obviously some of the
machine's states are undesirable to reach. 

To formalize the discussion the notion of a \texttt{protection state}
is introduced. Let $P$ be the set of \texttt{protection states} and $Q$
be a subset of $P$, where $\forall q \in Q$ are the states that the
system is authorized to enter, if the system is to be considered secure.

With the introduction of \texttt{protection states}, the problem is now
reduced to defining a method that will force the system to only make
transitions between states that are in the set $Q$.

\begin{figure}[!htpb]
\begin{center}
\includegraphics[width=0.5\textwidth]{images/statediagram.png}
\caption[A pictorial explanation of secure and insecure states]
{A five state situation. The directed arrows depict possible
transitions. It is an insecure system since it may reach an
insecure state}
\label{fig:statediagram}
\end{center}
\end{figure}


%%%%%%
\subsection{Definition of a secure system}
The follow definition is very general in nature and is quite intuitively
tied to the introduction of \texttt{protection states} above.

\begin{definition}
\label{definition:secure system}
\index{definition!secure system}
\index{secure system}
A \texttt{secure system} is a system that starts in an authorized state
and cannot enter an unauthorized state.
\end{definition}

This entirely encapsulates the example and the discussion in the
preceding section; the transitions that would render the state machine
describing the system entering an unauthorized state must be avoided if
a system is to remain secure.

An example of states and transitions between them is depicted in
Figure~\ref{fig:statediagram}. In the figure, states labeled ``1'',
``2'' and ``3'' are defined to be secure, while the states labeled ``4''
and ``5'' are defined to be insecure. The system described by these five
states, and the possible transitions between them, is not to be
considered secure since it is possible for the system to enter an
insecure state.

%%%%%%
\subsection{State transition control and the Access control matrix}
\index{access control matrix}
To solve the problem of which transitions can be allowed, some kind of
decision system that takes into account the current context and the
requested transition must be constructed. An appropriate model must be
able to determine exactly what actions a specific \texttt{subject} is
allowed to perform on any \texttt{object}.

A model that addresses these issues is a very intuitive model called the
\texttt{Access control matrix model}, which exhaustively describes the
rights that each \texttt{entity} have over all other 
\texttt{entities}~\cite{Bishop}.

The model partitions the entities of a system into two categories: the
entities that must be protected and those that don't. The entities that
are considered relevant to the protection state of the system are placed
into either a set of \texttt{objects} $O$ or a set of \texttt{subjects}
$S$, that is processes and users.
This makes it possible to associate all pair
$(s,o)$, where $s \, \in \, S$ and $o \, \in \, O$, with some
set of rights $r \, \subseteq \, R$, where $R$ is the set of all rights
available in the system. 

The right $r$ is then captured in an access matrix $A$ such
that $a[s,o] = \, r$, where $a[s,o] \, \in \, A$ and by
consequence $a[s,o] \, \subseteq \, R$.

\begin{figure}[!htpb]
\begin{center}
\begin{tabular}{l|l|l|l|l}
            & \textbf{file 1} & \textbf{file 2} & \textbf{process 1} &
            \textbf{process 2} \\
\hline
\textbf{process 1}   & read & read, write, own & read, write,    &    \\
                     &      &                  & execute, own    &    \\
\hline
\textbf{process 2}   & read, own & read & read & read, write,    \\
                     &           &      &      & execute, own    
\end{tabular}
\caption{An access control matrix describing the access rights for two
processes to two files and each other. Adapted from Bishop~\cite{Bishop}}
\label{figure:access control matrix}
\end{center}
\end{figure}

The three sets can be used to describe set of \texttt{protection states}
for the system using the triple $(S,O,A)$. That is, as long as the
identified \texttt{subjects}, accesses \texttt{objects} accordingly to
the rights given by the \texttt{access matrix} $A$, the system will
never enter an unauthorized state.

For example, consider the access control matrix depicted in 
Figure~\ref{figure:access control matrix}. It describes exactly which rights
``process 1'' and ``process 2'' has with respect to the files ``file 1''
and ``file 2'' and to each other. For example, ``process 1'' has no
rights over ``process 2,'' while the later may read from ``process 1.''

%%%%%%
\subsection{Protection states transitions}
\index{access control matrix!state transition}
In the previous section, the access control matrix was introduced. If
one assumes that such a matrix is made available, how can the actions
necessary to work with \texttt{objects} in a realistic way be done in
a secure manner? Those actions will necessary include: 
creation, deletion, modification and rights modification or rights
transfer for any object governed by the access matrix.

Bishop~\cite{Bishop} describes this as a series of state transitions, in
which the protection system changes. More specifically, if a
\texttt{system} starts in a state $X_0 \, = \, (S_0, O_0, A_0)$, and
then transitions through a set of states $X_1, \, X_2 \, \ldots$ by the
use of operations from an operation set $\{\tau_1, \, \tau_2, \, \ldots\}$,
then those transitions necessarily change the contents of the access
matrix if the access rights of \texttt{subjects} are affected, or if
\texttt{objects} are created or deleted. Obviously there is a need to
define the operations in the operation set 
$\{\tau_1, \, \tau_2, \, \ldots\}$ in such way that the access control
matrix won't be modified to allow system states that are considered
insecure.

These operations may be defined as commands. The definition of the
necessary commands has been well defined by previous work by Harrison
(among others)~\cite{Harrison}, and those specifications will be used
here. Some of the
precise notations are adapted from Bishop~\cite{Bishop}.

The context is such that before the execution of a \texttt{primitive
command} the system's state can be described by the triple $(S, O, A)$
and afterwards by the corresponding triple $(S', O', A')$. Special note
should be given to the preconditions and postconditions of the
aforementioned commands. The precondition presents the condition
relative to the system's state for the command to be able to execute,
and the postcondition describes the changes done to the access system's
state.

\begin{enumerate}
 \item \texttt{Primitive command}: \textbf{enter $r$ into a[s,o]} \\
       \texttt{Precondition}: The subject and object being
       considered exist in the access matrix \\
       \texttt{Postcondition}: If the right already exist in that
       entry, the command will not affect the matrix, else the right $r$
       is added

 \item \texttt{Primitive command}: \textbf{delete $r$ from a[s,o]} \\
       \texttt{Precondition}: The subject and object being
       considered exist in the access matrix \\
       \texttt{Postcondition}: If the right does not exist in the access
       matrix, nothing happens, else it is removed

 \item \texttt{Primitive command}: \textbf{create subject $s$} \\
       \texttt{Precondition}: The subject must not exist as a subject or an
       object before the execution of the command \\
       \texttt{Postcondition}: The subject is entered in the access matrix with
       previous entries having no rights in accessing the new entry. No
       access entries are added for the new subject either

 \item \texttt{Primitive command}: \textbf{destroy subject $s$} \\
       \texttt{Precondition}: The subject must exist in the access
       matrix \\
       \texttt{Postcondition}: The subject is removed from the access
       matrix, and all entries corresponding to the access rights of
       others relating to the removed object are also removed

 \item \texttt{Primitive command}: \textbf{create object $o$} \\
       \texttt{Precondition}: No such object exists \\
       \texttt{Postcondition}: Adds the object to the access matrix. Like the
       \textbf{create subject} command it does not manipulate the
       access rights present in the matrix

 \item \texttt{Primitive command}: \textbf{destroy object $o$} \\
       \texttt{Precondition}: The object must exist in the access matrix \\
       \texttt{Postcondition}: The object is removed from the access
       matrix and all rights in the access matrix relating to the
       object are also removed
\end{enumerate}

Using these command the access matrix will always be modified in such
way that the entries will be left in a consistent state.

However, to make use of these \texttt{primitive commands} to represent
most real world systems, more preconditions must be evaluated before any
of them are to be executed. For example, on most systems only the owner
of a file may enter or remove rights of a file. Also, many operations
group several \texttt{primitive commands} to do their job. A typical
example of such an operation is \textbf{creating a file}, which might do
the following:

\begin{enumerate}
 \item Does the user have the right to create contents in the directory
 of interest?
 \item Create the file, which is a \texttt{object}
 \item Set the owner of the file to the creating user
 \item Set default rights for everybody else on the newly created
 \texttt{object}
\end{enumerate}

Such grouping must be done for all commands that is done by an operating
system~\cite{Tanenbaum}, typically such commands are called system
calls.

Considering this new tool, can we be sure that the system is secure? Is
the transfer of rights between \texttt{subjects} concerning access to
other \texttt{subjects} and \texttt{objects} done in such a manner that
no rights are leaked and possibly exploitable by a malicious user?
This question is addressed in the next section.

\newpage
%%%%%%
\section{When is a system secure?}
\index{secure system}
In the previous sections the access matrix, and state transitions that
modify it, was introduced. Now the goal is to determine just how such
a transition can be made while ensuring that no rights are leaked in an
inconsistent manner, enabling the system to enter an insecure state.

This section starts with a light introduction to whether or not an
arbitrary \texttt{system} may be proved secure. The result of such a
proof presents the need for restriction of the transfer of rights in a
\texttt{system}. Such a restricted model for how rights are appropriately
transferred within an access matrix, to ensure that the \texttt{system}
does not enter an insecure state, is then presented.

%%%%%%
\subsection{Is a system generally provably secure?}
\index{secure system!proof}
A system's security is in the general case, unfortunately, proven to be
undecidable. Harrison and Ruzzo~\cite{Harrison} proved this in 1976 by
translating the actions of handling rights in an access control matrix
to the state transitions of a Turing machine, and setting the fact that
a right has been leaked in the access control matrix as the halting
state.

Since it has been shown that a Turing machine can not be proven to
reach its halting state, the problem is undecidable since it is
non--traceable.
%
(See e.g.~\cite{Sudkamp} for information about Turing machines and the
halting problem.)

%%%%%%
\subsection{A model for traceable transfer or rights}
\label{SPM}
\index{secure system!traceble}
\index{secure system!SPM}
\index{SPM|see{Schematic Protection Model}}
\index{Schematic Protection Model}
Even though it has been proved generally impossible to assert security in
system, a more controlled environment than the access control matrix
most general form will make it possible to guarantee that a system
will remain in a secure state. Sandhu demonstrated such a tool with the
Schematic Protection Model (\texttt{SPM})~\cite{Sandhu}, which is
proven to be traceable. The non--traceability of the access control
matrix is the focus of the problem of that model for general use.

\texttt{SPM} is made up of a few simple elements, which when
instantiated properly, are able to emulate other protection models. One
such model is the \texttt{Take grant model} (see~\cite{Bishop} for an
easy explanation of that model). \texttt{SPM} has the following
components:

\begin{enumerate}
 \label{list:spm}
 \item A finite set of principal types partitioned into two sets,
 holding subject's and object's type respectively

 \item A finite set of rights, which is partitioned into two sets. One
 holding the inert rights (the rights that do not alter the system's
 state) and another holding the control rights

 \item A finite collection of links predicates. Used to determine if
 there is a connection between two subjects, based on their types, that
 can be used to copy a right

 \item A filter function for each link predicate, which will either
 allow the copying of a right or deny it

 \item The operation for creating new subjects and objects

 \item A rule that is associated with all operations that create any
   type of entity, that control which initial rights the created
   entity will be associated with
\end{enumerate}

Note that \texttt{SPM} as presented only describe a monotonically growing
\texttt{system}.

Using this model, all rights are transfered using a well specified
system of rules that are unconditionally applied to all operations by
the links predicates and the filter functions.
Sandhu demonstrates several models in his paper by instantiating the
sets in the model's component list appropriately, and gives a 
convincing argument that many models can be emulated by \texttt{SPM},
and as such be traceable~\cite{Sandhu}.
The fact that \texttt{SPM} is so powerful and proven traceable, makes it
clear that models that are either equivalent with or instanciable in
\texttt{SPM} will be secure.

%%%%%%
\subsection{Conclusions concerning secure systems}
The above discussion made it clear that an unbound system is provably
insecure, which can be proven by mapping the primitive operations for
modifying an access matrix to a Turing machine. 

The introduction of
restrictive rules however, made it possible to limit the problem such
that it became traceable and thus provably secure. The proof of concept
provided was the Schematic Protection Model (\texttt{SPM}).

Since \texttt{SPM} is traceable, it must follow that if a system that
has a set of rules for access right transfer, which can be formulated with
the \texttt{SPM}, its security is traceable. In other words, if you can
express the system's rules in \texttt{SPM}, it is traceable, and hence
it can be proven secure; a finite number of operations are needed to
ensure that the system never enters an insecure state.

